/**************************************************************************
* File:            main.cpp	                                              *
* Description:	   Tests for 2sat.h and tarjan.h                          *
* Author:          Zhuk Artsem, 399                                       *
**************************************************************************/

#define _CRTDBG_MAP_ALLOC
#include <stdlib.h>
#include <crtdbg.h>

#include <iostream>
#include <vector>
#include <algorithm>
#include "graph.h"
#include "search.h"
#include "2sat.h"
#include "gtest\gtest.h"
#include "tarjan.h"
#include "graphgen.h"
#include "2satgen.h"
#include <stdlib.h>
#include <iostream>
#include <crtdbg.h>
#include <functional>

bool isValidSCC(std::vector<std::vector<int>> scc, Graph const * graph){
	int n = graph->getVerticesNumber();
	std::vector<std::vector<bool>> reachable(n, std::vector<bool>(n));

	for (int i = 0; i < n; ++i){
		std::vector<int> incidenceList = graph->getIncidenceList(i);
		for (auto &to : incidenceList)
			reachable[i][to] = true;
	}

	for (int i = 0; i < n; ++i)
		reachable[i][i] = true;

	for (int k = 0; k < n; ++k)
	for (int i = 0; i < n; ++i)
	for (int j = 0; j < n; ++j)
	if (reachable[i][k] && reachable[k][j])
		reachable[i][j] = true;

	std::vector<int> color(n);

	for (int i = 0; i<scc.size(); ++i)
	for (int vertex : scc[i])
		color[vertex] = i;

	for (int i = 0; i < n; ++i)
	for (int j = 0; j < n; ++j)
	if ((reachable[i][j] && reachable[j][i]) != (color[i] == color[j]))
		return false;

	return true;
}

bool fulfiled(std::vector<Disjunct> const &disjuncts, std::vector<bool> value){
	for (auto disjunct : disjuncts){
		int indexX = disjunct.x.index_;
		int indexY = disjunct.y.index_;
		if (!disjunct.isFulfiled(value[indexX], value[indexY]))
			return false;
	}
	return true;
}

bool hasSolution(int variables_number, std::vector<Disjunct> const &disjuncts){
	std::vector<bool> value(variables_number);
	int maxMask = 1 << variables_number;
	for (int mask = 0; mask < maxMask; ++mask){
		for (int j = 0; j < variables_number; ++j)
			value[j] = mask&(1 << j);
		if (fulfiled(disjuncts, value))
			return true;
	}
	return false;
}

bool isValidSolution(int variables_number, std::vector<Disjunct> const &disjuncts, std::vector<bool> value){
	if (!hasSolution(variables_number, disjuncts))
		return value.size() == 0;

	return fulfiled(disjuncts, value);
	
}

TEST(SCC, correctness){
	/* small graphs */
	for (int i = 1; i <= 5; ++i)
	for (auto &graph : getAllGraphs(i))
	if (!(isValidSCC(getSCC(graph.get()), graph.get()))){
		std::cout << "SCC brocken!\n";
		std::cout << "size " << i << "\n";
		for (int v = 0; v < i; ++v)
		for (int & to : graph->getIncidenceList(v))
			std::cout << v << " -> " << to << "\n";
		std::cout << "Components: \n";
		
		auto ans = getSCC(graph.get());
		for (auto &component : ans){
			for (auto &x : component)
				std::cout << x << " ";
			std::cout << "\n";
		}

		std::cout << "Have a good day!\n";

		return;
	}
	
	/* big graphs */

	int n = 300;

	for (int i = 0; i < 200; ++i){
		auto graph = getRandomGraph(n, 0.005*i);
		ASSERT_TRUE(isValidSCC(getSCC(graph.get()), graph.get()));
	}

}

TEST(SAT, correctness){
	/* small number of variables */

	for (int n = 1; n <= 4; ++n)
	for (auto &disjuncts : getAllInputs(n)){
		auto solution = get2SATSolution(n, disjuncts);
		if (!isValidSolution(n, disjuncts, solution)){
			std::cout << "Something wrong with 2SAT...\n";
			for (auto d: disjuncts){
				std::cout << d.x.index_*(d.x.desired_ ? 1 : -1) << " " << d.y.index_*(d.y.desired_ ? 1 : -1) << "\n";
			}
			std::cout << "My solution is : " << "\n";
			if (solution.size())
			for (auto &x : solution)
				std::cout << x << "\n";
			else
				std::cout << "I claim that there are no solution!\n";
			return ;
		}
	}

	/* big number of variables - 20*/

	int n = 20;

	for (int i = 0; i < n*n; ++i){
		auto disjuncts = getRandomInput(n, i);
		ASSERT_TRUE(isValidSolution(n, disjuncts, get2SATSolution(n, disjuncts)));
	}

}

TEST(Variable, getNumber){
	for (int i = 0; i < 100; ++i){
		int x = rand();
		int y = rand() & 1;
		ASSERT_EQ(Variable(x, y).getNumber(), 2 * x + y);
	}
}

TEST(Variable, isTrue){
	for (int i = 0; i < 100; ++i){
		int x = rand();
		int y = rand() & 1;
		int z = rand() & 1;
		ASSERT_EQ(Variable(x, y).isTrue(z), y == z);
	}
}

TEST(Disjunct, isFulfiled){
	for (int i = 0; i < 100; ++i){
		int x1 = rand();
		int x2 = rand();
		int v1 = rand() & 1;
		int v2 = rand() & 1;
		int y1 = rand() & 1;
		int y2 = rand() & 1;
		ASSERT_EQ(Disjunct(x1, v1, x2, v2).isFulfiled(y1, y2), (v1 == y1) || (v2 == y2));
	}
}

/* notVairble, variableNumber, isNegation are simple enought to not check them separately */
TEST(SAT, integation){
	for (int i = 0; i < 100; ++i){
		int x = rand();
		ASSERT_EQ(variableNumber(x), variableNumber(notVariable(x)));
	}
	for (int i = 0; i < 100; ++i){
		int x = rand();
		ASSERT_EQ(isNegation(notVariable(x)), (x & 1));
	}
}

TEST(SAT, make2SATGraph){
	/* small cases */
	for (int n = 1; n <= 3; ++n)
	for (auto &disjuncts : getAllInputs(n)){
		auto graph = make2SATGraph(n, disjuncts);
		std::vector<Edge> edges(0);
		for (auto &d : disjuncts){
			int index1 = d.x.getNumber();
			int index2 = d.y.getNumber();
			edges.emplace_back(notVariable(index1), index2);
			edges.emplace_back(notVariable(index2), index1);
		}
		ASSERT_EQ(*makeCompactGraph(edges, 2 * n), *graph);
	}

	/* big cases */

	int n = 300;

	for (int i = 0; i < n*n; ++i){
		auto disjuncts = getRandomInput(n, i);
		auto graph = make2SATGraph(n, disjuncts);
		std::vector<Edge> edges(0);
		for (auto &d : disjuncts){
			int index1 = d.x.getNumber();
			int index2 = d.y.getNumber();
			edges.emplace_back(notVariable(index1), index2);
			edges.emplace_back(notVariable(index2), index1);
		}
		ASSERT_EQ(*makeCompactGraph(edges, 2 * n), *graph);
	}
}

int main(int argc, char ** argv){
	::testing::InitGoogleTest(&argc, argv);
	srand(347);

	return RUN_ALL_TESTS();
}